l:IdLnk, L:IdLnk List, M:({l:IdLnk| (l  L) }MsgA).
(l  L)  (x, y:IdLnk. (x  L)  (y  L)  (M(x) ||+ M(y)))  M(l)  (mapl(l.M(l);L)) 

latex

Definitions	MsgA, (x  l), x:A. B(x), IdLnk, f(a), x(s), mapl(f;l), A ||+ B, (x,yL.P(x;y)), t  T, x:AB(x), {x:A| B(x) }, x.A(x), Type, P  Q, type List, Prop, (L), M1  M2, x,y. t(x;y), s = t, A & B, x:AB(x), x:A. B(x), P  Q, P & Q, P  Q
Lemmas	member-mapl, pairwise-mapl, ma-compat wf, ma-sub-join-list, mapl wf, msga wf, l member wf, IdLnk wf